Nuprl Lemma : insert-by-no-repeats 11,40

T:Type, eqr:(TT).
(ab:T. ((eq(a,b)))  (a = b))
 Linorder(T;a,b.(r(a,b)))
 (x:TL:(T List).
 sorted-by(x,y(r(x,y));L no_repeats(T;L no_repeats(T;insert-by(eq;r;x;L))) 
latex


Definitionstype List, t  T, s = t, Type, x:AB(x), x:AB(x), Linorder(T;x,y.R(x;y)), b, sorted-by(R;L), no_repeats(T;l), P  Q, f(a), , x.A(x), x,yt(x;y), P  Q, , insert-by(eq;r;x;l), P & Q, x:A  B(x), P  Q, [car / cdr], S  T, |g|, A, #$n, {x:AB(x)} , l[i], ||as||, [], , , A  B, {i..j}, a < b, (x  l), Void, False, ff, b, p =b q, i <z j, i j, (i = j), x =a y, null(as), a < b, , x f y, =, a < b, =, =, [d], p  q, p  q, p q, tt, Unit, left + right, if b then t else f fi , A List, xLP(x), P  Q, <ab>, AntiSym(T;x,y.R(x;y)), Trans(T;x,y.E(x;y)), Refl(T;x,y.E(x;y)), Connex(T;x,y.R(x;y)), Order(T;x,y.R(x;y)), case b of inl(x) => s(x) | inr(y) => t(y)
Lemmasmember-insert-by, false wf, cons member, sorted-by-cons, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, no repeats cons, insert-by wf, l member wf, length wf2, select wf, int seg wf, not wf, nat wf, bool wf, iff wf, linorder wf, no repeats wf, assert wf, sorted-by wf

origin